COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00011 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb NOTES ON RESEARCH TOPICS, ESPECIALLY FOR THESES


	I am prepared to supervise research in the following topics,
although I am also willing to consider other topics proposed by
students.  Which of these topics would lead to PhD theses will
require work by the student.  In many of them, the student would have
to contribute substantially to the definition of the problem as
well as to finding a solution.

SYSTEM PROGRAMMING

	It would be hard to persuade me to supervise the design of
a new programming language or design an operating system as
a thesis project.  There would really have to be a new idea
and not merely a dissatisfaction with the details of present
implementations.  Instead I would prefere to see research in
new areas such as the following:

.item←0
#. Information description.  Many files exist that
are accessible to our computer over the ARPAnet or by
telephone.  Develop a language for describing a class of
such files that would permit a program to answer a question
by extracting the information from such a file.  Easy (I hope)
example:  many ARPAnet sites have telephone directories in
their computer as do we.  These directories all have approximately
the same information but have different file formats.
Devise a way of describing such files so that a single program
can find addresses and telephone numbers from any of the files
using the description of that file.

	The description should also permit putting information
into the file.  Preferably it should be possible to describe the
file partially, so that if the M.I.T. phone file normally has
some weird entry like our BAM allocation, we wouldn't have to
know about it in order to read or change a file or to create a
new one.  In the last case, there would probably have to be a
default given.

	It is important to understand that we are talking about
describing existing files that other people have created according
to their own tastes and not a shiny new file system that would
conquer the world.

	Many files are not directly readable and modifiable.  Instead
they are parts of information systems designed for direct human
use.  In order that a computer could extract information from or
put information into such a file, it would need a description
of the system of interaction.  One such file, accessible over the
ARPAnet is the Lawrence Berkeley Lab file of census data.
A file description system that would permit programs to answer questions
about this file once it has been described would be a substantial
achievement.  To play fair, the description system should be designed
before the designer sees the manual for the LBL data base.

#. Implement core war. See COREWA[S77,JMC].

#. Business communication language.  See CBCL[f75,jmc].

THEORY OF ARTIFICIAL INTELLIGONCE

#. Minimal models of a collection of sentences
	See me for an oral spiel, but first read minima[f75,jmc].

#. Finitization.  A possible scheme for showing certain sentences
satisfiable by translating them into theories in which satisfiability
means satisfiability in models of a fixed size.  See finiti[f75,jmc].

MATHEMATICAL THEORY OF COMPUTATION

#. Proving intensional properties of programs

	A property of a program is extensional if it is a propoerty
of the function computed by the program, i.e. a property of the
input-output relation.  Intensional properties include the time
and space used, the number of recursive calls, etc.  Our approach
to intensional properties is to make them extensional properties
of related or "derived" programs.  Ben Moszkowski has done some of
this, and some techniques are given in McCarthy and Talcott
LISP: Programming and Proving.  We have concentrated on functional
programs.  When the program is the fixed point of a computable
functional, then some intensional properties of the program are
extensional properties of the functional.  Which properties are
extensional properties of the functional remain to be seen.
Conjecture:  If the function is strict, then the number of recursions
required to evalueate the function for given arguments is an
extensional property of the program.  Indeed the set of evaluations
should be an extensional property as should a certain evaluation
tree.  The sequence of evaluations will not be an extensional
property of the functional.

#. Blobs

	A blob is a piece of flowchart with many entries and exits.
They can be glued together to make larger blobs and are characterized
by certain functions.  It would be interesting to know if the
Yanov decision procedures are consequences of functional manipulation
of blob functions.  See the file
BLOB[W76,JMC] 19-Feb-77	THE BLOB FUNCTIONS OF FLOW CHARTS
for more information.

#. First order theory of "cons should not evaluate its arguments"

	In a well-known report Daniel Friedman and 
David Wise argue that cons should be programmed as an FSUBR that
merely conses its formal arguments without evaluating them.  This
enlarges the LISP data structures to include objects like the
list of all integers.  Their evaluator won't evaluate it when it
occurs in a computation but merely evaluates expands as required
when tests or printing make it necessary.  Friedman and Wise suggested
to me that part of the extension required to treat thes objects
logically is to make cons(bottom,bottom) ≠ bottom, cons(A,bottom)≠bottom.
This isn't all, by any means.  Obviously, the S-expressions have to
be extended to include some computable infinite S-expressions.  Can
this still be done in first order logic, and what kind of a theory
do we get?  Is it good for anything or just a curiosity?